| Definitions | x:A B(x), s = t, Knd, d-decl(D;i), d-world-state(D;i),  x:A. B(x), left+right, P  Q, P & Q, x:A  B(x), Dsys, Feasible(D), Id, {x:A| B(x) },  ,  x:A. B(x), Unit, Type, IdLnk, locl(a), M.da(a), P   Q, False,  A, A B,  , #$n, n-m, d-comp(D;v;sched;dec), CV(F), f(a), 1of(t), M(i), M.init(x)?v,  x.A(x), i= j, if b t else f fi, M.state, t  T, {i..j }, Prop,  b, b,  , P  Q, State(ds), -n, n+m, a<b, Void, S  T, i j < k, S  T, hd(l), let x = a in b(x), d-partial-world(D;f;t';s), World, queue(l;t), Msg, ||as||, destination(l), i = j, ij, p q, True, i<j, p  q,  T, P Q, doact(k;v), i j, mtag(m), rcv(l,tg), Msg(M), w.M, mval(m), M.dout(l,tg), {T}, tag(k), lnk(k), act(k), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), w-action-dec(TA;M;i), a = b, mlnk(m), source(l), <a,b>, MsgA, stutter-state(s), next-world-state(D;i;s;k;v), Case b of inl(x) s(x) ; inr(y) t(y), M.ds(x), M.ef(k,x,s,v)?w, M.din(l,tg), M.Msg, type List, M.sends(k,s,v), null, inr(x), s ~ t, f(x)?z |
| Lemmas | subtype rel list, filter type, mlnk wf d, ma-msg wf, ma-send-val wf, doact wf, d-decl-subtype, ma-ef-val wf, mval wf, d-decl wf, next-world-state wf, stutter-state wf, ma-dout wf, msga wf, lsrc wf, mlnk-hd-w-queue, assert-d-eq-Loc, assert-eq-id, eq id wf, not rcv locl, rcv one one, Knd wf, rcv wf, hd wf, assert of band, and functionality wrt iff, assert of lt int, bnot thru band, squash wf, true wf, bnot of lt int, assert of bor, or functionality wrt iff, assert of le int, band wf, lt int wf, bor wf, le int wf, d-eq-Loc wf, ldst wf, length wf1, w-Msg wf, w-queue wf, subtype rel self, world wf, d-partial-world wf, ifthenelse wf, CV wf, le wf, ma-init-val wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf, d-comp wf2, int seg wf, d-world-state wf, d-feasible wf, ma-da wf, locl wf, ma-st wf, d-m wf, nat wf, IdLnk wf, Id wf, unit wf, dsys wf, nat properties |
dec:(i,a:Id